es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C, e:E.
 [e: sndr is_ack  rcvr]
  (e':{a:E| [a: sndr is_req   rcvr]} . f2f+-pred(e',ff.Sender(sndr,e)))) 

latex

Definitions

loc(e), <a, b>, Id, s = t, x:A. B(x), b, Void, x:AB(x), P  Q, False, A, x:A  B(x), ES, FIFO, F2F+-decls, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ff.C, t.1, E, f(a), @i(x:T), Dec(P), let x,y = A in B(x;y), P  Q, A r B, {T}, isrcv(e), t  T, Atom$n, Type, P & Q, P  Q, ff.R, A c B, vartype(i;x), , [e: i p j], (e < e'), [e: i p j], plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack), x:A. B(x), ff.S, is_ack , is_req  , owes_ack , awaiting , {x:A| B(x)} , f2f+-pred(e',e), ff.Sender, , state@i, for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes), left + right, P  Q, e c e'

Lemmas

snd-it wf, f2f+-pred wf, ack-has-f2f+-pred, fifoSender wf, snd-it-of-rcv-it, rcv-it wf, plus-ify wf, f2f+Req wf, f2f+Ack wf, f2f+Wait wf, f2f+Owes wf, fifoC wf, fifoR wf, es-E wf, fifoS wf, F2F+-decls wf, FIFO wf, event system wf, f2f+-property, es-isrcv-loc, equal functionality wrt subtype rel, es-loc-pred